\section{Future Work}
The following list gives an overview of possible future enhancements to the
Muen separation kernel:

\begin{itemize}
	\item Covert/Side-Channel analysis
	\item Cache coloring
	\item Linux virtualization
	\item Hardware passthrough/PCIe virtualization
	\item APIC virtualization
	\item Policy writer support tools
	\item Dynamic resource management
	\item Performance testing \& optimization
	\item Power Management
	\item Multicore subjects
	\item Formal verification
	\item Fully virtualized subjects/Windows virtualization
\end{itemize}

The following sections describe some of the more interesting items.

\subsection{Covert/Side-Channel Analysis}
Since the main purpose of a separation kernel is the isolation of subjects, any
unintended channel that enables information flow must be prohibited or at least
reduced to an acceptable data rate.

The first step in preventing such flows is to identify potential covert and
side-channels in the kernel to determine the strength of the isolation. This
includes a systematic and thorough analysis of the scheduler and the underlying
hardware platform. Special care must be taken to evaluate the interaction of the
kernel with the hardware since minor differences in interpretation of the
specification can lead to unintended side-effects. A very deep knowledge and
understanding of the Intel x86 architecture is required for such an analysis.

A guide to covert channel analysis was published as part of the "Rainbow
Series", a set of computer security standards and guidelines, termed Light Pink
Book \cite{LightPinkBook}.

\subsubsection{Cache Coloring}
A well-known source of high-bandwidth side-channels are processor caches
\cite{cryptoeprint:2005:271}. One method to prevent this channel is called
\emph{cache coloring}. The main concept is to partition the cache into disjoint
groups and assign a color to each of the groups. This mechanism has been
presented in literature in the context of real-time systems for more than 15
years \cite{Liedtke:1997:OCP:523983.828369}
\cite{Mueller:1995:CSS:216633.216677}.

In a second step each subject is associated with a color. All subjects of a
given color share the same cache partition. In turn subjects of differing color
have no access to identical cache locations, which means the cache cannot be
used as a side-channel.

This mechanism could be implemented by extending the policy compilation tool
without changes to the kernel.

\subsection{Linux Subject}
Porting the Linux kernel to run as a subject on the Muen separation kernel would
enable the execution of a large number of Linux user-space applications. This
would drastically increase the number of real world use-cases, that a system
using the Muen kernel could be applied to.

Leveraging the VM profile, which allows a subject to perform memory management
via EPT (see section \ref{subsubsec:ept}), reduces the porting effort. Changes
to the Linux boot process are needed, since it is quite involved. The Linux
kernel implements an architecture-dependent boot protocol that is explained as
part of the kernel documentation\footnote{See Linux sources:
Documentation/x86/boot.txt}.

Combined with the \emph{hardware passthrough} enhancement, Linux could be used
to control virtually any PCI(e) device. This would add the abundant hardware
support of the Linux kernel to systems based on the separation kernel, with a
comparably small increase in kernel complexity.

\subsection{Hardware Passthrough/PCIe Virtualization}
Even though the separation kernel has support for resources, that can be
accessed using port and memory-mapped I/O, newer hardware devices are attached
to a PCI bus. Prior to their usage, such devices must be configured using a
mechanism called the \emph{PCI configuration space}. Since this resource allows
to (re-)configure PCI devices, the kernel must be in charge of device
management like initial setup.

Subjects performing device enumeration to discover the PCI topology would need
a virtualized view of the PCI bus or be altered to not perform disallowed access
to PCI resources.

Additional measures need to be implemented to enable subject assignment and safe
usage of PCI devices. Most PCI devices support Direct Memory Access (DMA), which
allows them to directly access all data in physical memory. Secondly, a PCI
device is not restricted to a specific hardware interrupt but can be instructed
to trigger any interrupt. Intel's VT-d technology, as briefly mentioned in
section \ref{subsubsec:vtd}, provides mechanisms to implement the necessary
isolation functions.

Implementing these enhancements using VT-d should keep the kernel complexity at
an acceptable level.

\subsection{APIC Virtualization}\label{subsec:apicv}
Currently pending events that are to be injected into subjects are stored in
per-subject data structures, that are protected by a spinlock. This is
sub-optimal since having to acquire locks when handling interrupts is not very
efficient.

Intel provides an advanced hardware virtualization feature called APIC
virtualization (APICv\index{APICv}) that could greatly improve Muen's event
handling, see Intel SDM, volume 3C, chapter 29.

By giving subjects access to a virtualized APIC, VM exits related to interrupt
processing are greatly reduced. The processor emulates access to the APIC by
tracking the state of the virtual APIC, and delivering virtual interrupts all in
VMX non-root mode without the need for a trap. The associated data structure,
called posted-Interrupt descriptor, is accessed using atomic operations, which
makes locks and the current pending events list unnecessary. This would further
simplify interrupt processing in the Muen kernel.

The current implementation of the separation kernel does not support APICv, due
to the limited availability of hardware supporting this advanced processor
feature.

\subsection{Policy Writer Support Tools}
The policy of a Muen kernel based system plays a very important role. Since the
kernel simply enforces a given policy, the policy writer is responsible for the
correctness of the system specification.

Currently, to write a policy the system integrator has to edit an XML file
directly. While the \texttt{skpolicy} tool performs validation checks to catch
obvious configuration mistakes, it is an error-prone process.

A graphical tool would greatly simplify this process by providing a more
intuitive method for policy authoring. Visualizing key parts of the policy
would be very beneficial. The generation of diagrams representing the
information flows between subjects based on their shared resources or graphical
illustration of scheduling plans are two examples, how such a tool could assist
in policy validation.

\subsection{Dynamic Resource Management}
Currently, resource management is static and there is little flexibility. All
system parameters must be explicitly declared in the policy. Switching between
predefined scheduling plans is the only property changeable at runtime. While
this allows to tightly control and validate a system via the policy, all
assigned resources are indispensable even though some of them may not be in use
during a particular period.

For example, a system consisting of multiple different VM subjects with their
respective operating systems need multiple gigabytes of memory when running.
In a static system configuration, all the assigned memory is committed and
reserved even though only one of the VMs might be in operation. A system
providing dynamic resource management could greatly improve the usage of
hardware resources.

This can be achieved by extending the trusted $\tau$0 subject. It has the same
trust-level as the kernel and forms part of the TCB. Via an appropriate
interface, it can update parts of the policy and instruct the kernel to enforce
the changes.

\subsection{Formal Verification}
By implementing the kernel in SPARK and proving the absence of runtime errors,
we have shown that the kernel is free from exceptions. While these proofs
provide some evidence to the correctness claim of the implementation, the
application of these particular formal methods do not provide any assurances
beyond the error free execution of the kernel. Proving functional properties
such as the correspondence of the scheduler to a given formal specification is
necessary to further raise the confidence in systems based on the Muen kernel.

A link between the SPARK tool suite and the interactive proof assistant
Isabelle/HOL exists in the form of the HOL-SPARK tool. Isabelle would allow to
prove the formal correctness of the Muen separation kernel.
